COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Abstract: Computation processes are described in the restricted Elephant
C00005 00003	.draft←true
C00006 00004	#. Expressing a sequential program in Elephant
C00012 00005		The above Elephant formalism sorts the program
C00018 ENDMK
C⊗;
Abstract: Computation processes are described in the restricted Elephant
formalism by giving the values of the variables at time %2t+1%1 as
explicit functions of their values at time ⊗t.  Including a "program
counter" among these dependent variables leads to a direct representation
of a "flowchart program" ⊗P as a sentence of first order logic.  Combining
several flowcharts is accomplished by taking the conjunction of their
sentences.

	Properties of programs are expressed and proved in terms of the
sentence ⊗P together with the axioms for the data domain.  No special
axioms for programming are required, and proof methods like inductive
assertions, subgoal induction and intermittent assertions are just
particular techniques of proof within first order logic.  Several useful
kinds of equivalence of programs are readily defined.

	Explicit use of a time variable seems to be more powerful
and more straightforward than any form of temporal logic.

	General Elephant programs express the values of the variables
at time ⊗t as functions of the whole past, and this sometimes permits
specifying processes without specifying data structures for remembering
the data.  This is a step towards giving programming languages more
of the power of natural languages.
.draft←true
.if draft then begin nofill

contents

introduction
example and its expression sorted by variable and by pc
formalism
relation to functional formalisms
further examples
equivalence
proofs
comparison with other formalisms
parallel processes
general elephant
remarks
references

.end
#. Expressing a sequential program in Elephant
.a←item

	Consider the following Algol 60 program fragment (declarations
are omitted) for doing multiplication by addition:

.begin nofill
%2

entry:	i := n;				∂(30)0
	p := 0;				∂(30)1
loop:	qif i = 0 qthen qg exit;	∂(30)2
	i := i - 1;			∂(30)3
	p := p + m;			∂(30)4
	qg loop;			∂(30)5
.end

The corresponding Elephant program consists of the equations

.begin nofill
.zz←12
%2

∀t.[entry ≤ pc(t) ≤ entry+5 ⊃

i(t+1) →=_∂(zz)IF pc(t) = entry THEN n
∂(zz)ELSE IF pc(t) = entry+3 THEN i(t) - 1
∂(zz)ELSE i(t)

∧

p(t+1) →=_∂(zz)IF pc(t) = entry+1 THEN 0
∂(zz) ELSE IF pc(t) = entry+4 THEN p(t) + m
∂(zz)ELSE p(t)

∧

pc(t+1) →=_∂(zz)IF pc(t) = entry+2 ∧ i(t) = 0 THEN exit
∂(zz)ELSE IF pc(t) = entry+5 THEN entry+2
∂(zz)ELSE pc(t) + 1].
.end

	In these equations ⊗i(t) and ⊗p(t) replace the simple
variables of the Algol program.  The function ⊗pc(t) is the
program counter, and it takes values from %2entry+0%1 to %2entry+5%1,
corresponding
to the numbers written on the right of the Algol program.  It should
be apparent from the example that any program made up of assignments
and qgs can be systematically translated to an Elephant program.
We have used the logical conditional expression %2IF_..._THEN_..._ELSE%1
rather than qif_..._qthen_..._qelse, because there is no reason to
provide for an undefined case.  (The distinction is discussed in
(Cartwright and McCarthy 1979)).
If the reader is a reactionary and
refuses to admit conditional expressions as terms in first order
logic, then they can be eliminated.

	Notice also that the length of the Elephant program is linear in the
length of the Algol program.

	Having one value of ⊗pc(t) for
each statement in the Algol program is unnecessary, although it makes
the systematic character of the translation more apparent.  If we
let %2pc(t)_=_entry%1 correspond to the initialization, ⊗pc(t)_=_entry+1
correspond to the loop, then the equations become

.begin nofill
.zz←12
%2

∀t.(pc(t) = entry ∨ pc(t) = entry+1 ⊃

i(t+1) →=_∂(zz)IF pc(t) = entry THEN n
∂(zz)ELSE IF pc(t) = entry+1 ∧ i(t) ≠ 0 THEN i(t) - 1
∂(zz)ELSE i(t)

∧

p(t+1) →=_∂(zz)IF pc(t) = entry THEN 0
∂(zz) ELSE IF pc(t) = entry+1 ∧ i(t) ≠ 0 THEN p(t) + m
∂(zz)ELSE p(t)

∧

pc(t+1) →=_∂(zz)IF pc(t) = entry+1 THEN [IF i(t) = 0 THEN exit ELSE entry+1]
∂(zz)ELSE pc(t) + 1].
.end

	The correctness of the first version of the Elephant program is
given by the sentence

	%2∀m n t0.[pc(t0) = entry ⊃ ∃t1.[t1 > t0 ∧ pc(t1) = exit ∧ p(t1) = mn
∧ ∀t.[t0 ≤ t ≤ t1 ⊃ entry ≤ t ≤ entry + 5]]]%1.

The statement is provable from any first order axiomatization of arithmetic
together with ⊗P0 itself.  No special
axioms for programs or "logic of programs" is required.

	Thus an entirely conventional mathematical way of writing
recursion equations leads to a convenient programming language.  One might be
tempted to call the language Algol 50, since it only uses ideas that
were familiar in 1950.

	The proof of correctness for this
multiplication program is misleadingly simple, since
we can easily write explicit formulas for ⊗i(t), ⊗p(t), and
⊗pc(t) and prove them by mathematical induction.  More typical proofs
occur when it isn't convenient to give explicit formulas for the
variables as functions of time or for the value of ⊗t for which the
program terminates.  Then the computational content of the proof is
is often essentially the same as that of an %2inductive assertions%1 proof
combined with induction on a rank function of the variables taking
values in a suitable inductively ordered set.

	The above Elephant formalism sorts the program
by variables, while a sequential program sorts it according to the program
counter.  The latter is more conventional and often more convenient.

	The pc-sorted version of the previous program is

.begin nofill
.zz←12

%2
∀t.[entry ≤ pc(t) ≤ entry + 5 ⊃
∂(zz)IF pc(t) = entry THEN i(t+1) = n
∂(zz)ELSE IF pc(t) = entry+1 THEN p(t+1) = 0
∂(zz)ELSE IF pc(t) = entry+2 THEN pc(t+1) = (IF i(t) = 0 THEN EXIT ELSE entry+3)
∂(zz)ELSE IF pc(t) = entry+3 THEN i(t+1) = i(t) - 1
∂(zz)ELSE IF pc(t) = entry+4 THEN p(t+1) = p(t) + m
∂(zz)ELSE IF pc(t) = entry+5 THEN pc(t+1) = entry+2

∂(zz)ELSE pc(t+1) = pc(t) +1 ∧ i(t+1) = i(t) ∧ p(t+1) = p(t)%1

.end

	Notice that there is one clause for each statement in the Algol
program and an additional clause giving the default rules for updating

	Now suppose ⊗P2 is another program involving some of the same
same variables as ⊗P1 and possibly some others, and suppose we
want to combine these programs so that ⊗P2 is executed after ⊗P1.
We need only take the conjunction of the sentences together with
a sentence like %2entry2_=_exit1%1.  Should we want to do so, we
can transform the conjunction into an equivalent sentence which
has the same form as ⊗P1 or ⊗P2.

	The method of combination by conjunction works the same
in more complicated cases.  A program can have multiple entries
and exits, any exit can be connected to any entry just by equating
suitable ⊗entry and ⊗exit parameters.